\begin{tabbing}
$\forall$\=$k$:Knd, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$a$:Knd fp$\rightarrow$ Type, $f$:(Id$\times$Top) List, $k_{1}$:Knd, $l_{1}$:IdLnk,\+
\\[0ex]$d_{1}$:$x$:Id fp$\rightarrow$ Type, $d_{2}$:$a$:Knd fp$\rightarrow$ Type, $f_{1}$:(Id$\times$Top) List.
\-\\[0ex]${\it ds}$ $\parallel$ $d_{1}$
\\[0ex]$\Rightarrow$ ${\it da}$ $\parallel$ $d_{2}$
\\[0ex]$\Rightarrow$ $\neg$$\langle$$k$$,\,$$l$$\rangle$ $=$ $\langle$$k_{1}$$,\,$$l_{1}$$\rangle$
\\[0ex]$\Rightarrow$ (\=with declarations \+
\\[0ex]ds:${\it ds}$
\\[0ex]da:${\it da}$
\\[0ex]$k$(v) sends $f$ s v on link $l$
\\[0ex]$\Vert\!+$ \=with declarations \+
\\[0ex]ds:$d_{1}$
\\[0ex]da:$d_{2}$
\\[0ex]$k_{1}$(v) sends $f_{1}$ s v on link $l_{1}$)
\-\-
\end{tabbing}